Bitwise opcode spec (AND, OR, XOR) #50
Conversation
|
@miha-stopar @ChihChengLiang We have addressed previous comments. PTAL |
specs/opcode/17OR.md
Outdated
| - stack_pointer + 1 | ||
| - pc + 1 | ||
| - gas + 3 | ||
|
|
There was a problem hiding this comment.
I think some lookups are needed, like:
- first operand must come from the first element in the stack
- second operand must come from the second element in the stack
- result is at the new top of the stack
specs/opcode/17OR.md
Outdated
| 1. stack underflow: when stack is empty | ||
| 2. gas out: remaining gas is not enough | ||
| ```python | ||
| class Stack(): |
There was a problem hiding this comment.
Not sure why Stack code is needed here?
src/zkevm_specs/opcode/bitwise.py
Outdated
| a8s = [1] | ||
| b8s = [4] | ||
| c8s = [0] | ||
| check_xor(a8s, b8s, c8s) |
There was a problem hiding this comment.
| check_xor(a8s, b8s, c8s) | |
| check_and(a8s, b8s, c8s) |
src/zkevm_specs/opcode/bitwise.py
Outdated
| a8s = [1] | ||
| b8s = [4] | ||
| c8s = [5] |
There was a problem hiding this comment.
len(a8s) is 1, how come the test pass for this?
specs/opcode/16AND.md
Outdated
| - stack_pointer + 1 | ||
| - pc + 1 | ||
| - gas + 3 | ||
|
|
There was a problem hiding this comment.
Would like to see more descriptions of how the opcode is checked in the circuit so that the reviewers/auditors know better how to review the circuit code. For example,
"We have two inputs a and b and an output c, all are EVM words. We break the EVM word into 32 bytes, lookup an AND table of 1-byte inputs, and apply the lookup to the 32 chunks of each a, b, and c to see if a[i] | b[i] === c[i] holds for i in 0~31"
|
@miha-stopar Could you approve running workflows as well? Thank you. |
Done. |
specs/opcode/16AND_17OR_18XOR.md
Outdated
|
|
||
| `a`, `b`, and `c` are all EVM words. We break three EVM words into 32 bytes and | ||
| apply the lookup to the 32 chunks of `a`, `b`, and `c` to see if | ||
| `a[i] OP b[i] == c[i]` holds for `i = 0..31`, where `OP` belongs to |
There was a problem hiding this comment.
If using rust's range style, it should be 32 or =31, right? Since there are some other cases are using 0..31, so I think we should avoid such ambiguity.
| `a[i] OP b[i] == c[i]` holds for `i = 0..31`, where `OP` belongs to | |
| `a[i] OP b[i] == c[i]` holds for `i = 0..32`, where `OP` belongs to |
specs/opcode/16AND_17OR_18XOR.md
Outdated
| - `b` is at the second position of the stack | ||
| - `c`, the result, is at the new top of the stack | ||
| - Apply the lookup to 32 tuples of `a, b, c` chunks, | ||
| `(a[i], b[i], c[i]), i = 0..31`, with opcode corresponding table |
There was a problem hiding this comment.
ditto
| `(a[i], b[i], c[i]), i = 0..31`, with opcode corresponding table | |
| `(a[i], b[i], c[i]), i = 0..32`, with opcode corresponding table |
No description provided.